the_es:event_system{i:l}, e:es-E(the_es).
((es-isrcv(the_es; e)))  (es-acttype(the_es; e)  Type) 

latex

Definitions	t  T, x:A. B(x), kind(e), isrcv(k), x:AB(x), P  Q, P  Q, x:A  B(x), P  Q, P  Q, b, A, act(k), Id, loc(e), f(a), es_info(es), es-kind(es; e), es-act(es; e), loc(e), es-V(es), es-acttype(es; e), es-isrcv(es; e), es-E(es), event_system{i:l}, Type
Lemmas	event system wf, loc wf, Id wf, actof wf, not wf, assert wf, islocal-not-isrcv, assert of bnot, isrcv wf, kind wf